\begin{tabbing}
w{-}machine{-}constraint($w$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:Id.\+
\\[0ex]let ${\it Choose}$,${\it Trans}$,${\it Send}$ = w{-}machine($w$;$i$) in 
\\[0ex]$\forall$$t$:$\mathbb{N}$.
\\[0ex]$\neg$w{-}isnull($w$; w{-}a($w$; $i$; $t$))
\\[0ex]$\Rightarrow$ \=($\lambda$$x$.w{-}s($w$; $i$; ($t$+1); $x$))\+
\\[0ex]$=$
\\[0ex]${\it Trans}$(w{-}kind($w$; w{-}a($w$; $i$; $t$)),w{-}val($w$; w{-}a($w$; $i$; $t$)),$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$))
\\[0ex]$\in$ $x$:Id$\rightarrow$w{-}vartype($w$; $i$; $x$)
\\[0ex]\& (\=islocal(w{-}kind($w$; w{-}a($w$; $i$; $t$)))\+
\\[0ex]$\Rightarrow$ \=isl(${\it Choose}$(act(w{-}kind($w$; w{-}a($w$; $i$; $t$))),$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$)))\+
\\[0ex]\& \=w{-}val($w$; w{-}a($w$; $i$; $t$))\+
\\[0ex]$=$
\\[0ex]outl(${\it Choose}$(act(w{-}kind($w$; w{-}a($w$; $i$; $t$))),$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$)))
\\[0ex]$\in$ w{-}valtype($w$; $i$; w{-}a($w$; $i$; $t$)))
\-\-\-\\[0ex]\& \=w{-}m($w$; $i$; $t$)\+
\\[0ex]$=$
\\[0ex]${\it Send}$(w{-}kind($w$; w{-}a($w$; $i$; $t$)),w{-}val($w$; w{-}a($w$; $i$; $t$)),$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$))
\\[0ex]$\in$ Msg($w$.M) List
\-\-\-
\end{tabbing}